COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.cb MODAL KNOWLEDGE AXIOMS AND THEIR TRANSLATION TO FIRST ORDER LOGIC


	Around 1960 I developed a modal system of
axioms for knowledge but put off publishing, because I couldn't
solve the problem of proving non-knowledge.  However,
  I presented it in my seminar in Kyoto in 1975
and it was much further developed by Sato, Hayashi and Igarashi who
developed several improvements and extensions.  In particular, Sato's
thesis (1977) gave it a Kripke style semantics, in terms of which proving
non-knowledge could be done in some cases.
It is now worth describing in
connection with the relation between modal systems of axioms and
their translation into ordinary first order logic.

	⊗S knows ⊗p, where ⊗S is a person and ⊗p is a sentence,
is denoted by %2S*p%1.  There is a special person called "any fool"
denoted by 0.  The sentences are built up from propositional constants
using the logical operators and the knowledge operators, ⊗S1*, ⊗S2*, etc.
where ⊗S1, ⊗S2, etc. are constants denoting persons.

	We sometimes use the abbreviation %2Sα$p%1 for %2S*p_∨_S*¬p%1
and read it "⊗S knows whether ⊗p".

	Three systems called KTM, KT4, and KT5 are defined.
Each of them has all instances of the following schemata as axioms
and modus ponens as the sole rule of inference.

.nofill
K:	0*π (where π is any instance of a propositional calculus tautology
including those formed using ⊗S*); Any fool knows tautologies.

K0:	%2S*p ⊃ p; What someone knows is true.

K1:	0*(S*p ⊃ p); Any fool knows the above.

K2:	0*(0*p ⊃ 0*S*p); Any fool knows that what any fool knows, any fool
knows everyone knows.

K3:	0*(S*p ∧ S*(p ⊃ q) ⊃ S*q)%1; Any fool knows that anyone can do modus ponens.

	KT4 has the additional schema
%2
K4:	0*(S*p ⊃ S*S*p); Any fool knows that if someone knows something, he
knows he knows it.

	KT5 has the additional schema

K5:	0*(¬S*p ⊃ S*(¬S*p))%1; Any fool knows that if someone doesn't know
something, he knows he doesn't know it.

	The following facts about these systems have been proved by
various people:

	1. If 0 is the only individual, then the schemata K, K0, ... K3 give
a system equivalent to the modal system S5, where ⊗0*p is read
"⊗p is necessary".

	2. The theorems of KTM, KT4, and KT5 involving a single person
letter (say ⊗S1) that is not 0 correspond to the theorems of the modal
systems M, S4, and S5 respectively.

	3. If K5 is present, then K4 can be omitted.  This corresponds
to the fact that S4 is included in S5.

	4. We can axiomatize the puzzle of the three wise men in the
following way.